Section: New Results

Probabilistic Analysis

Participants : Patrick Cousot, Michaël Monerau.

The abstract interpretation theory has been widely used in the past decades for verifying properties of computer systems. We have introduced a new extension of this well-known framework to the case of probabilistic systems [21] .

The probabilistic abstraction framework we propose allows to systematically lift any classical analysis or verification method to the probabilistic setting by separating in the program semantics the probabilistic behavior from the (non-)deterministic behavior. This separation provides new insights for designing novel probabilistic static analyses and verification methods.

We have defined concrete probabilistic semantics and proposed different ways to abstract them. The approach is expressive and effective. The previous techniques for probabilistic analysis are actually abstractions expressible in our framework.